package probsym;

import java.util.HashMap;
import java.util.LinkedList;
import java.util.HashSet;
import java.util.Map;

import gov.nasa.jpf.jvm.Verify;
import gov.nasa.jpf.symbc.Debug;
import gov.nasa.jpf.symbc.probsym.Analyze;

public class BinomialHeapBug2{

	// internal class BinomialHeapNode
	public static class BinomialHeapNodeBug /*implements java.io.Serializable*/{
		//private static final long serialVersionUID=6495900899527469811L;

		private int key; // element in current node

		private int degree; // depth of the binomial tree having the current node as its root

		private BinomialHeapNodeBug parent; // pointer to the parent of the current node

		private BinomialHeapNodeBug sibling; // pointer to the next binomial tree in the list

		private BinomialHeapNodeBug child; // pointer to the first child of the current node

		public BinomialHeapNodeBug(int k) {
			//	public BinomialHeapNode(Integer k) {
			key = k;
			degree = 0;
			parent = null;
			sibling = null;
			child = null;
		}

		public int getKey() { // returns the element in the current node
			return key;
		}

		private void setKey(int value) { // sets the element in the current node
			key = value;
		}

		public int getDegree() { // returns the degree of the current node
			return degree;
		}

		private void setDegree(int deg) { // sets the degree of the current node
			degree = deg;
		}

		public BinomialHeapNodeBug getParent() { // returns the father of the current node
			return parent;
		}

		private void setParent(BinomialHeapNodeBug par) { // sets the father of the current node
			parent = par;
		}

		public BinomialHeapNodeBug getSibling() { // returns the next binomial tree in the list
			return sibling;
		}

		private void setSibling(BinomialHeapNodeBug nextBr) { // sets the next binomial tree in the list
			sibling = nextBr;
		}

		public BinomialHeapNodeBug getChild() { // returns the first child of the current node
			return child;
		}

		private void setChild(BinomialHeapNodeBug firstCh) { // sets the first child of the current node
			child = firstCh;
		}

		public int getSize() {
			return (1 + ((child == null) ? 0 : child.getSize()) + ((sibling == null) ? 0
					: sibling.getSize()));
		}

		private BinomialHeapNodeBug reverse(BinomialHeapNodeBug sibl) {
			BinomialHeapNodeBug ret;
			if (sibling != null)
				ret = sibling.reverse(this);
			else
				ret = this;
			sibling = sibl;
			return ret;
		}

		private BinomialHeapNodeBug findMinNode() {
			BinomialHeapNodeBug x = this, y = this;
			int min = x.key;

			while (x != null) {
				if (x.key < min) {
					y = x;
					min = x.key;
				}
				x = x.sibling;
			}

			return y;
		}

		// Find a node with the given key
		private BinomialHeapNodeBug findANodeWithKey(int value) {
			BinomialHeapNodeBug temp = this, node = null;
			while (temp != null) {
				if (temp.key == value) {
					node = temp;
					break;
				}
				if (temp.child == null)
					temp = temp.sibling;
				else {
					node = temp.child.findANodeWithKey(value);
					if (node == null)
						temp = temp.sibling;
					else
						break;
				}
			}

			return node;
		}

	}

	// end of helper class BinomialHeapNode

	//--------------------------------------------------------------------

	private static Map<Integer,Integer> coveredSet = new HashMap<Integer,Integer>();
	
	public static void covered(int br) {
			Analyze.coverage(""+br);		
	}

	public static void coveredRandom(int br) {		
		Integer cov = coveredSet.get(br);
		if (cov == null) {
			cov = 0;
		}
		coveredSet.put(br, cov+1);				
	}

	
	public static void gen(int br, BinomialHeapNodeBug n1, BinomialHeapNodeBug n2) {//SPECIFY
		covered(br);
		//coveredRandom(br);
		
	}

	//-------------------------------------------------------------------

	private BinomialHeapNodeBug Nodes;

	private int size;
	private int sizeShadow;

	public BinomialHeapBug2() {
		Nodes = null;
		size = 0;
		sizeShadow = 0;
	}

	boolean repOk() {
		final LinkedList seen = new LinkedList();

		if (this.Nodes != null) {

			// son aciclicos los hijos del head?
			if (!isAcyclic(this.Nodes, seen))
				return false;

			// esta ordenado el arbol que cuelga de head ?
			if (!ordered(this.Nodes))
				return false;

			// el parent del head es null ?
			if (this.Nodes.parent != null)
				return false;

			// si hay un sibling, el degree del head es menor
			if (this.Nodes.sibling != null) {
				if (this.Nodes.degree >= this.Nodes.sibling.degree)
					return false;
			}

			// ns son siblings del head
			BinomialHeapNodeBug ns = this.Nodes.sibling;
			;
			while (ns != null) {

				// son aciclicos los hijos del sibling del head
				if (!isAcyclic(ns, seen))
					return false;

				// es parent del sibling del head es null ?
				if (ns.parent != null)
					return false;

				// el degree de este sibling es menor al del siguiente ?
				if (ns.sibling != null) {
					if (ns.degree >= ns.sibling.degree)
						return false;
				}

				// estan ordenados el subarbol que cuelga de este sibling ?
				if (!ordered(ns))
					return false;

				// proximo sibling del head
				ns = ns.sibling;
			}

		}

		System.out.println("this size " + this.size + " =  seen " + seen.size());
		
		if (this.size != seen.size())
			return false;

		return true;
	}

	/**
	 * retorna true si es acyclico el subarbol y paso, - verifica que parent
	 * esta bien formado - chequea que degree sea positivo - que element sea
	 * non_null (si element es Object) - que degree sea la cantidad de hijos (no
	 * descendientes) del nodo
	 */
	private boolean isAcyclic(final BinomialHeapNodeBug start, final LinkedList seen) {

		if (seen.contains(start))
			return false;

		if (start.degree < 0)
			return false;

		// enable these lines if element is instance of Object
		// if (start.element==null)
		// return false;

		seen.add(start);

		BinomialHeapNodeBug child = start.child;

		int child_count = 0;

		while (child != null) {

			child_count++;

			if (child.parent != start)
				return false;

			if (!isAcyclic(child, seen))
				return false;

			if (child.sibling != null) {
				if (child.degree <= child.sibling.degree)
					return false;
			}
			child = child.sibling;
		}

		if (start.degree != child_count)
			return false;

		if (start.child != null) {
			int tam_child = 1;
			if (start.child.child != null) {
				BinomialHeapNodeBug curr = start.child.child;
				while (curr != null) {
					tam_child += count_nodes(start.child.child);
					curr = curr.sibling;
				}
			}

			int tam_sibling = 1;
			if (start.child.sibling != null) {
				BinomialHeapNodeBug curr = start.child.sibling;
				while (curr != null) {
					tam_sibling += count_nodes(start.child.sibling);
					curr = curr.sibling;
				}
			}

			if (tam_child != tam_sibling)
				return false;

		}

		return true;
	}

	private boolean ordered(final BinomialHeapNodeBug node) {
		if (node.child != null) {
			if (node.child.key < node.key) {
				return false;
			}
			if (!ordered(node.child)) {
				return false;
			}
			for (BinomialHeapNodeBug ns = node.child.sibling; ns != null; ns = ns.sibling) {
				if (ns.key < node.key) {
					return false;
				}
				if (!ordered(ns)) {
					return false;
				}
			}
			return true;
		}

		return true;

	}

	BinomialHeapNodeBug helper_minimum() {
		if (this.Nodes == null)
			return null;
		else
			return this.Nodes.findMinNode();
	}

	private int count_nodes(BinomialHeapNodeBug start) {

		int node_count = 1;

		BinomialHeapNodeBug child = start.child;
		while (child != null) {

			node_count += count_nodes(child);

			child = child.sibling;
		}

		return node_count;
	}
	
	
	// 2. Find the minimum key
	public int findMinimum() {
		return Nodes.findMinNode().key;
	}

	// 3. Unite two binomial heaps
	// helper procedure
	private void merge(BinomialHeapNodeBug binHeap) {
		BinomialHeapNodeBug temp1 = Nodes, temp2 = binHeap;
		while ((temp1 != null) && (temp2 != null)) {
			if (temp1.degree == temp2.degree) {
				gen(1, temp1, temp2);
				BinomialHeapNodeBug tmp = temp2;
				temp2 = temp2.sibling;
				tmp.sibling = temp1.sibling;
				temp1.sibling = tmp;
				temp1 = tmp.sibling;
			} else {
				if (temp1.degree < temp2.degree) {
					if ((temp1.sibling == null)
							|| (temp1.sibling.degree > temp2.degree)) {
						gen(2, temp1, temp2);
						BinomialHeapNodeBug tmp = temp2;
						temp2 = temp2.sibling;
						tmp.sibling = temp1.sibling;
						temp1.sibling = tmp;
						temp1 = tmp.sibling;
					} else {
						gen(3, temp1, temp2);
						temp1 = temp1.sibling;
					}
				} else {
					BinomialHeapNodeBug tmp = temp1;
					temp1 = temp2;
					temp2 = temp2.sibling;
					temp1.sibling = tmp;
					if (tmp == Nodes) {
						gen(4, temp1, temp2);
						Nodes = temp1;
					} else {
						gen(5, temp1, temp2);
					}
				}
			}
		}

		if (temp1 == null) {
			temp1 = Nodes;
			while (temp1.sibling != null) {
				gen(6, temp1, temp2);
				temp1 = temp1.sibling;
			}
			temp1.sibling = temp2;
		} else {
			gen(7, temp1, temp2);
		}
	}

	// another helper procedure
	private void unionNodes(BinomialHeapNodeBug binHeap) {
		merge(binHeap);

		BinomialHeapNodeBug prevTemp = null, temp = Nodes, nextTemp = Nodes.sibling;

		while (nextTemp != null) {
			if ((temp.degree != nextTemp.degree)
					|| ((nextTemp.sibling != null) && (nextTemp.sibling.degree == temp.degree))) {
				gen(8, temp, nextTemp);
				prevTemp = temp;
				temp = nextTemp;
			} else {
				if (temp.key <= nextTemp.key) {
					gen(9, temp, nextTemp);
					temp.sibling = nextTemp.sibling;
					nextTemp.parent = temp;
					nextTemp.sibling = temp.child;
					temp.child = nextTemp;
					temp.degree++;
				} else {
					if (prevTemp == null) {
						gen(10, temp, nextTemp);
						Nodes = nextTemp;
					} else {
						gen(11, temp, nextTemp);
						prevTemp.sibling = nextTemp;
					}
					temp.parent = nextTemp;
					temp.sibling = nextTemp.child;
					nextTemp.child = temp;
					nextTemp.degree++;
					temp = nextTemp;
				}
			}
			gen(12, temp, nextTemp);

			nextTemp = temp.sibling;
		}
	}

	// 4. Insert a node with a specific value
	public void insert(int value) {
		if (value > 0) {
			BinomialHeapNodeBug temp = new BinomialHeapNodeBug(value);
			if (Nodes == null) {
				Nodes = temp;
				size = 1;
				sizeShadow = 1;
			} else {
				unionNodes(temp);
				size++;
				sizeShadow++;
			}
		}
		//else {
		//	covered(101);
		//}
	}

	// 5. Extract the node with the minimum key
	public int extractMin() {
		if (Nodes == null)
			return -1;

		BinomialHeapNodeBug temp = Nodes, prevTemp = null;
		BinomialHeapNodeBug minNode = Nodes.findMinNode();
		while (temp.key != minNode.key) {
			gen(13, temp, prevTemp);
			prevTemp = temp;
			temp = temp.sibling;
		}

		if (prevTemp == null) {
			gen(14, temp, prevTemp);
			Nodes = temp.sibling;
		} else {
			gen(15, temp, prevTemp);
			prevTemp.sibling = temp.sibling;
		}
		temp = temp.child;
		BinomialHeapNodeBug fakeNode = temp;
		while (temp != null) {
			gen(16, temp, prevTemp);
			temp.parent = null;
			temp = temp.sibling;
		}

		if ((Nodes == null) && (fakeNode == null)) {
			gen(17, temp, prevTemp);
			size = 0;
		} else {
			if ((Nodes == null) && (fakeNode != null)) {
				gen(18, Nodes, fakeNode);
				Nodes = fakeNode.reverse(null);
				size = Nodes.getSize();
			} else {
				if ((Nodes != null) && (fakeNode == null)) {
					gen(19, Nodes, fakeNode);
					size = Nodes.getSize();
				} else {
					gen(20, Nodes, fakeNode);
					unionNodes(fakeNode.reverse(null));
					size = Nodes.getSize();
				}
			}
		}

		sizeShadow--;
		return minNode.key;
	}

	// 6. Decrease a key value
	public void decreaseKeyValue(int old_value, int new_value) {
		BinomialHeapNodeBug temp = Nodes.findANodeWithKey(old_value);
		if (temp == null)
			return;
		temp.key = new_value;
		BinomialHeapNodeBug tempParent = temp.parent;

		while ((tempParent != null) && (temp.key < tempParent.key)) {
			int z = temp.key;
			gen(21, temp, tempParent);
			temp.key = tempParent.key;
			tempParent.key = z;

			temp = tempParent;
			tempParent = tempParent.parent;
		}
	}

	// 7. Delete a node with a certain key
	public void delete(int value) {
		if ((Nodes != null) && (Nodes.findANodeWithKey(value) != null)) {
			decreaseKeyValue(value, findMinimum() - 1);
			extractMin();
		}
	}

	public static void findBug() {
		BinomialHeapBug2 b = new BinomialHeapBug2();
		b.insert(14);
		b.insert(14);
		b.insert(14);
		b.insert(14);
		b.insert(13);
		b.insert(13);
		b.insert(13);
		b.insert(13);
		b.insert(14);
		b.insert(14);
		b.insert(14);
		b.insert(14);
		b.insert(14);
		//b.extractMin();
		//b.extractMin();
		b.delete(13);
		
		if (b.size == b.sizeShadow)
			System.out.println("Fine");
		else 
			System.out.println("Broken");
		
		b.delete(13);
		int min = b.findMinimum();
		System.out.println("min = " + min);
		//assert b.repOk();
	}
	
	public static void runTest(int[] options, int limit) {
		BinomialHeapBug2 b = new BinomialHeapBug2();
		//extension

//		b.insert(Debug.makeSymbolicInteger("p0"));
//		
//		b.insert(Debug.makeSymbolicInteger("p1"));
//		
//		b.insert(Debug.makeSymbolicInteger("p2"));
//		
//		b.insert(Debug.makeSymbolicInteger("p3"));		
//		
//		b.insert(Debug.makeSymbolicInteger("p4"));
//				
//		b.insert(Debug.makeSymbolicInteger("p5"));
//		b.insert(Debug.makeSymbolicInteger("p6"));
//		b.insert(Debug.makeSymbolicInteger("p7"));
//		b.insert(Debug.makeSymbolicInteger("p8"));
//		b.insert(Debug.makeSymbolicInteger("p9"));
//		b.insert(Debug.makeSymbolicInteger("p10"));	
//		
//		b.insert(Debug.makeSymbolicInteger("p11"));
//		//b.insert(Debug.makeSymbolicInteger("p12"));	
//		
//		b.extractMin();
//		if (b.size != b.sizeShadow) {
//			b.covered(99);
//		}
//		else {
//			b.covered(100);
//		}
//		assert b.size == b.sizeShadow : "1 size mismatch actual = " + b.size + " expected = " + b.sizeShadow;
/*		
		b.extractMin();
		
		if (b.size != b.sizeShadow)
			b.covered(999);
		
		assert b.size == b.sizeShadow : "2 size mismatch actual = " + b.size + " expected = " + b.sizeShadow;
		
		*/
		
		int round = 0;
		while (round < limit) {
			if (options[round] == 1) {
				//System.out.println("Insert v1");
				b.insert(options[limit + round]);
			}
			else {
				//System.out.println("Delete v1");
				b.delete(options[limit + round]);
				//b.insert(options[limit + round]);
				//b.extractMin();
			}
			//else if (options[round] == 2) {
			//	//System.out.println("ExtractMin round 1");
			//	b.extractMin();
			//}	
						
			round++;
			if (b.size != b.sizeShadow)
				b.covered(99);
			//assert b.size == b.sizeShadow : " size mismatch actual = " + b.size + " expected = " + b.sizeShadow;
//			Verify.ignoreIf(BinomialHeapBugSymmetryCheck.symmetryCheck(b.Nodes));
		}
		
	}
	
	public static void runTestDriver(int length) {
		int[] values = new int[length*2];
		int i = 0;
		while (i < 2*length) {
			if (i < length)
				values[i] = Debug.makeSymbolicInteger("c" + i);
			else 
				values[i] = Debug.makeSymbolicInteger("v" + i);
			i++;
		}
	    runTest(values,length);
	}
	
	public static void runRandomTest(int length, int range) {
		int[] values = new int[length*2];
		int i = 0;
		while (i < 2*length) {
			if (i < length) {
				values[i] = (new java.util.Random()).nextInt(2)+1;
			}
			else { 
				values[i] = (new java.util.Random()).nextInt(range);
			}
			i++;
		}
	    runTest(values,length);
	}
	
	public static void randomTestDriver(int length, int range, int repeat) {
		for (int i = 0; i < repeat; i++) {
			runRandomTest(length,range);
		}
		for (Map.Entry<Integer, Integer> e : BinomialHeapBug2.coveredSet.entrySet()) {
			System.out.println(e.getKey() + " " + e.getValue());
		}
	}
	
	public static void main(String[] Argv) {
		//findBug();
		runTestDriver(2);
		//randomTestDriver(4,100,1000);
		
		/*
		BinomialHeap b = new BinomialHeap();

		b.insert(3);
		b.insert(5);
		System.out.println("min: " + b.findMinimum());
		System.out.println("size: " + b.size);
		b.extractMin();
		System.out.println("min: " + b.findMinimum());
		*/
	}
	
	/*
	public static void main(String[] Argv) {
		BinomialHeapBug b = new BinomialHeapBug();
		b.insert(14);
		b.insert(14);
		b.insert(14);
		b.insert(14);
		
		System.out.println(b.size + " - " + b.sizeShadow);
		
		b.insert(13);
		b.insert(13);
		b.insert(13);
		b.insert(13);
		
		System.out.println(b.size + " - " + b.sizeShadow);
		
		b.insert(14);
		b.insert(14);
		b.insert(14);
		b.insert(14);
		b.insert(14);
		
		System.out.println(b.size + " - " + b.sizeShadow);
		
		b.extractMin();
		
		System.out.println(b.size + " - " + b.sizeShadow);
		
		b.extractMin();
		
		System.out.println(b.size + " - " + b.sizeShadow);
		
		if (b.repOk())
			System.out.println("Fine");
		else 
			System.out.println("Broken");
		
		int min = b.findMinimum();
		
		System.out.println(min);

		b.insert(3);
		b.insert(5);
		System.out.println("min: " + b.findMinimum());
		System.out.println("size: " + b.size);
		b.extractMin();
		System.out.println("min: " + b.findMinimum());
	
		
		
		
	}
*/
}
// end of class BinomialHeap
